%!TEX root = paperEdit.tex
\section{Conclusions and Future Work}
\label{sec:conclusions}

\ncomment{We have presented REPROVE, a proof-of-concept system for automatically
analyzing the low-level communication protocol of a smart-card, 
 by reasoning over a formal model of the ISO
7816 standard,
regardless of the protocol's implementation. 
We have
used REPROVE to successfully extract at least one model from each
tested card and shown that, although 
analyzing proprietary implementations is a combinatorial problem, it
is possible to leverage background knowledge to effectively reduce the
search space. To the best of our knowledge, REPROVE is the first
system that successfully reverse-engineers proprietary
implementations.
REPROVE's results can
provide the necessary evidence to reason about the implementation of
the protocol and discover possible security flaws. Obtaining such
evidence is especially crucial, as bad implementations may lead to
fraud and/or disputes between card issuer and client.}{simples 2 paragraphs se mia}
  

\ncomment{We focused on the \func{C\_logIn} function, which authorizes
  access to and operations over sensitive data. Compromising the
  \func{C\_logIn} function enables man-in-the-middle attacks to other
  cryptographic functions as well. The \func{C\_logIn} function is a
  robust proof of concept. Though analyzing further functions is
  certainly in our current and future work, doing so will merely
  reinforce our results.}{why c_login (reviewer's comment)} As a
starting point we have provided evidence by reverse-engineering
another function (\func{C\_generateKey}). The results suggest that our
methodology is indeed strong enough to be used for the general case.
\eat{ The
  analysis results suggested that the cards implemented trivial
  methods of authentication. Additionally, none of the tested cards
  respected the RSA PKCS\#11 requirement of assigning session handles
  to freshly initiated sessions. Finally two of the cards sent the PIN
  in plain text. Naturally, findings like the above can be used as
  strong evidence for deciding whether the card is vulnerable to
  attacks. }
  
\ncomment{REPROVE addresses PKCS\#11 attacks at the APDU layer. PKCS\#11 defines
specifications for secure implementations and applies to a broad range
of cards. These specifications have to be addressed at the
communication layer as well, \eg in session identification. REPROVE's
analysis exposed several violations of the standard's specifications.
Reaching these findings in the first place would not have been
possible without reverse-engineering. We therefore believe our
approach cuts across all layers of the PKCS\#11 implementation and
provides a blueprint that can be applied to other models and protocols
as well.}{attacks found, flexibility, other protocols (reviewer's comment)}


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "paperEdit"
%%% End: 
